<html>
<head><meta charset="utf-8"><title>Function implementations that  need to satisfy invariants · t-lang · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/index.html">t-lang</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html">Function implementations that  need to satisfy invariants</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="241645697"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645697" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645697">(Jun 05 2021 at 16:58)</a>:</h4>
<p>I was looking at <a href="https://github.com/rust-lang/rust/issues/86027">https://github.com/rust-lang/rust/issues/86027</a> and in particular <a href="https://github.com/rust-lang/rust/blob/master/library/std/src/rt.rs#L22-L53">these functions</a>. Now, the thing is that these functions must satisfy certain constraints to be sound (e.g. not panic), but this is not at all reflected anyway with <code>unsafe</code>, which surprised me somewhat.</p>
<p>I then realised that we don't really have a way in the language to signal this – do we? <code>unsafe fn</code> only signals that the caller must maintain some sort of invariants imposed by the callee; And here we kind of want the reverse.</p>
<p>cc <span class="user-mention" data-user-id="310399">@Mara</span></p>



<a name="241645817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645817">(Jun 05 2021 at 17:01)</a>:</h4>
<p>In theory, they could be declared as an impl of some unsafe trait.</p>



<a name="241645822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645822">(Jun 05 2021 at 17:01)</a>:</h4>
<p>This somewhat reminds me of the desire to declare that certain attributes are "unsafe" (like <code>no_mangle</code>) (been trying to find the issue for this for a while)</p>



<a name="241645844"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645844" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mara <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645844">(Jun 05 2021 at 17:02)</a>:</h4>
<p>yeah we have <code>unsafe impl</code> for that i guess</p>



<a name="241645889"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645889" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mara <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645889">(Jun 05 2021 at 17:02)</a>:</h4>
<p>but things get a bit weird when we get to functions at the edge of rust/std, like <code>lang = start</code> etc.</p>



<a name="241645895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241645895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241645895">(Jun 05 2021 at 17:02)</a>:</h4>
<p>but practically, a dependence on safe code having some particular implementation is not uncommon</p>



<a name="241646221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241646221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mara <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241646221">(Jun 05 2021 at 17:09)</a>:</h4>
<p><code>lang</code> items are pretty much just 'trait impl's, in that they are already defined (incl. requirements) and only fill in the implementation of something.</p>



<a name="241646628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241646628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241646628">(Jun 05 2021 at 17:19)</a>:</h4>
<p><span class="user-mention" data-user-id="123586">@nagisa</span> how's this different from unsafe code using a safely implemented data structure and relying on its functional correctness?<br>
we dont expact that data structure to have any special marker either, do we?</p>



<a name="241646641"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241646641" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241646641">(Jun 05 2021 at 17:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="123586">nagisa</span> <a href="#narrow/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants/near/241645822">said</a>:</p>
<blockquote>
<p>This somewhat reminds me of the desire to declare that certain attributes are "unsafe" (like <code>no_mangle</code>) (been trying to find the issue for this for a while)</p>
</blockquote>
<p>I dont see the relationship; <code>no_mangle</code> is unsafe in the sense that it can cause UB...<br>
your functions are "super-safe" in that they guarantee more than the bare minimum "will not cause UB and return well-formed results from well-formed inputs"</p>



<a name="241646796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241646796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241646796">(Jun 05 2021 at 17:22)</a>:</h4>
<p><code>#[lang]</code> in this instance imposes requirements on the function that's annotated with the attribute, but this fact is not signaled in any way. I'm not sure what you're trying to say with the datastructure analogy.</p>



<a name="241647066"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241647066" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241647066">(Jun 05 2021 at 17:28)</a>:</h4>
<p>Oh, sorry, I might have mixed this up with another very similar recent discussion</p>



<a name="241647210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241647210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bstrie <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241647210">(Jun 05 2021 at 17:32)</a>:</h4>
<blockquote>
<p>lang items are pretty much just 'trait impl's, in that they are already defined (incl. requirements) and only fill in the implementation of something.</p>
</blockquote>
<p>could perhaps replace the start lang item with <code>unsafe impl Rust { fn start() -&gt; isize { ...</code>, equivalently magic but expresses the existence of an implementor-upheld safety invariant?</p>



<a name="241660503"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Function%20implementations%20that%20%20need%20to%20satisfy%20invariants/near/241660503" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Function.20implementations.20that.20.20need.20to.20satisfy.20invariants.html#241660503">(Jun 05 2021 at 23:10)</a>:</h4>
<p>I've had to have this for interrupt handlers on the GBA: the function pointer must point to an <code>a32</code> coded function, but rust doesn't have a way to enforce that in the type system.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>